2 links tagged with all of: formal verification + security
Click any tag below to further narrow down your results
Links
Anthropic's Frontier Red Team used Claude, with Theorem Labs, to prove security properties across more than a hundred real open-source libraries in a few weeks. The point is that formal verification, which used to be limited to small codebases or required heavy expert time, may now be practical at scale.
- Formal verification can prove code is free of certain classes of bugs, but has historically been limited to small codebases or costly expert effort.
- Claude was used to prove security properties in over one hundred real-world open-source libraries over a span of a few weeks.
- The work was done in collaboration with Theorem Labs, and the full research is on Anthropic's site.
AWS introduced the Nitro Isolation Engine on its new M9g and M9gd Graviton5 instances and used Isabelle/HOL to prove that it enforces strict VM isolation. They modeled the engine in a subset of Rust (μRust), wrote Separation Logic specifications, and proved functional correctness, memory safety, and noninterference to guarantee confidentiality and integrity.
- AWS deployed a formally verified hypervisor component (Nitro Isolation Engine) into production commercial cloud infrastructure for the first time, on new M9g/M9gd Graviton5 instances.
- They produced 330,000 lines of machine-checked Isabelle/HOL proofs, matching seL4's verification scale, covering functional correctness, memory safety, and noninterference.
- The proof approach modeled the engine in a custom μRust subset (no traits/dynamic dispatch) with Separation Logic specs and a weakest-precondition calculus via their open-source AutoCorrode library.
- Every guest-state-touching operation must pass through this engine, which checks requests against the formal spec to mathematically guarantee VM confidentiality and integrity.